Quiz (Week 4)

1. Minimal Specifications
- 1.1. Question 1
- 1.2. Question 2
2. Data Invariants
- 2.1. Question 3
- 2.2. Question 4
3. Data Refinement
- 3.1. Question 5
4. More on Testing Properties

1 Minimal Specifications

1.1 Question 1

Let gcd :: Int -> Int -> Int denote the function that returns the greatest common divisors of its inputs. The gcd function satisfies the following list of properties for all nonnegative input numbers x and y:

p1 x y = gcd x y == gcd y x
p2 x = gcd x 0 == gcd x x
p3 x y = gcd x (x * y) == gcd x x
p4 x y = gcd x (gcd y x) == gcd x y
p5 x = gcd x 1 == gcd 1 1

However, running tests for all of these properties takes too long for the impatient programmer. This is because many of these properties are logically redundant. If property A logically implies property B, then testing for property B is unlikely to fail when testing for property A has already passed.

Choose a subset of the properties above that, together with the usual laws of arithmetic involving addition and multiplication, imply all of the others, but do not contain any redundant properties.

Hint: Think about possible implementations of a function f that would fail the above properties. If you can't write an implementation that fails a given property but passes all of the others, it's a good indication that the property is redundant.

✗p3 alone,
✗p1 and p2,
✗p1, p2 and p3,
✔p1, p3 and p4,
✗p1, p3 and p5,
✗p1, p2, p3, p4 and p5.

Property 3 alone cannot imply all the others: the function f x y == x satisfies f x (x * y) == x == f x x, but clearly does not satisfy the analogue of property 1, f x y == f y x.

Properties 1, 2 and 3 cannot imply all the others: the function f x y = if even x && even y then 1 else 0 satisfies both f x y == f y x, f x 0 == f x x and f x (x * y) = f x x, but not f x (f y x) == f x y, because f 2 (f 1 2) == f 2 0 == 1, while f 2 1 == 0.

In the set of properties 1, 3 and 5, number 5 is redundant. We show this using equational reasoning.

  gcd x 1
== -- by p1
  gcd 1 x
== -- by arithmetic x == 1 * x
  gcd 1 (1 * x)
== -- by p3 with x := 1
  gcd 1 1

We already know properties 1 and 3 imply the 5th, but not the 4th, so all we need to verify is that properties 1, 3 and 4 imply the 2nd. Again, we can use equational reasoning

  gcd x 0
== -- by x * 0 == 0
  gcd x (x * 0)
== -- by p3 with y := 0
  gcd x x

1.2 Question 2

Here's a standard (inefficient) reverse function for lists, and a collection of QuickCheck properties to specify it.

rev :: [Int] -> [Int]
rev (x:xs) = rev xs ++ [x]
rev []     = []

prop_1 :: [Int] ->  Bool
prop_1 xs = length (rev xs) == length xs

prop_2 :: [Int] -> [Int] -> Bool
prop_2 xs ys = rev (xs ++ ys) == rev ys ++ rev xs

prop_3 :: [Int] -> Int -> Bool
prop_3 xs x = count x xs == count x (rev xs)
  where
    count x xs = length (filter (== x) xs)

Which of the above properties is redundant given the other two?

✔prop_1
✗prop_2
✗prop_3
✗None of the above.

Property 3 essentially says that the output of reverse is a permutation of its input. Given that, we already know that the lengths will be the same. Thus property 1 is redundant.

2 Data Invariants

We have decided to represent undirected graphs using adjacency matrices. For example, a graph of four nodes arranged in a rectangle:

0 ----- 1
|       |
|       |
2 ----- 3

Would be represented as the matrix:

type Graph = [[Bool]]

m :: Graph
m = [[False, True,  True,  False],
     [True,  False, False, True ],
     [True,  False, False, True ],
     [False, True,  True,  False]]

That is, the value (m !! a) !! b is True iff the node numbered a is connected to the node numbered b.

2.1 Question 3

Select all data invariants that should apply to our Graph type, assuming g :: Graph:

✔transpose g == g
✗all or g
✔all (\x -> length x == length g) g
✗map reverse g == g

In order to be an adjacency matrix, the number of rows and columns must be equal, hence property 3 is needed. To represent an undirected graph, the transpose of the matrix must be equal to the original matrix (it is diagonally symmetrical), hence property 1. The second property is meaningless and not true if you have a node disconnected from all others. The fourth property also holds for our example, but not in general (for example if node 1 is not connected to node 3).

2.2 Question 4

We have the following graph operations:

newGraph :: Int -- number of nodes
         -> Graph
newGraph n = replicate n (replicate n False)

connected :: Graph -> (Int, Int) -> Bool
connected g (x, y) | x < length g && y < length g = (g !! x) !! y 
                   | otherwise                    = False

connect :: (Int, Int) -> Graph -> Graph
connect (x, y) = modify y (modify x (\_ -> True)) . modify x (modify y (\_ -> True))
  where
    modify :: Int -> (a -> a) -> [a] -> [a]
    modify 0 f (x:xs) = f x : xs
    modify n f (x:xs) = x : modify (n - 1) f xs
    modify n f []     = []

We have defined a wellformedness predicate for our data invariants, called wellformed. Select the properties we should assert about our operations¹.

✔wellformed (newGraph n)
✗wellformed (connect x y g) ==> wellformed g
✗wellformed (connect x y g)
✔wellformed g ==> wellformed (connect x y g)

The third property does not necessarily apply, if the input graph is not well formed. The second property may apply in this case, but it is not necessary nor sufficient to show our data invariants are preserved.

The other properties states that outputs are wellformed when inputs are wellformed, which is correct.

3 Data Refinement

We now build a different model, where we think of our graph as a pair of an edge list and an integer counting the overall number of nodes in the graph.

data Model = M Int [(Int, Int)]

newGraphA :: Int -> Model
newGraphA n = M n []

connectedA :: Model -> (Int, Int) -> Bool
connectedA (M n es) (x,y) = (x,y) `elem` es

connectA :: (Int, Int) -> Model -> Model
connectA (x, y) (M n es) 
  | x < n && y < n = M n ((x,y):(y,x):es)
  | otherwise      = M n es

3.1 Question 5

Which one of these relations holds between our Model and Graph data types precisely if they represent the same graph?

✗

ref :: Graph -> Model -> Bool
ref g (M n es) = length g == n
              && all (\(x,y) -> (g !! x) !! y) es

✗

ref :: Graph -> Model -> Bool
ref g (M n es) = all (\(x,y) -> ((x,y) `elem` es) == ((g !! x) !! y))
                     [(x,y) | x <- [0..n-1], y <- [0..n-1]]

✗

ref :: Graph -> Model -> Bool
ref g (M n es) = length g == n 
              && any (\(x,y) -> ((x,y) `elem` es) == ((g !! x) !! y))
                     [(x,y) | x <- [0..n], y <- [0..n]]

✔

ref :: Graph -> Model -> Bool
ref g (M n es) = length g == n 
              && all (\(x,y) -> ((x,y) `elem` es) == ((g !! x) !! y))
                     [(x,y) | x <- [0..n-1], y <- [0..n-1]]

The first answer only looks at edges that are in the abstract graph. It would allow edges to be present in the matrix but not in the abstract graph. The second answer does not ensure that the number of nodes in the two graphs are the same. The third answer uses any rather than all, and its bounds are off by one. The fourth answer is correct.

4 More on Testing Properties

4.1 Question 6

Consider the gcd function from Question 1. Define the function

f :: Int -> Int
f = gcd 2

Which of the following testing strategies can be used to test f?

✗Invertibility
✗Involution
✔Idempotence
✗All of the above

The operation f is not invertible, since f 2 == 2 and f 4 == 2. Thus, 1 cannot be used. Since being involutive is a special case of being invertible, 2 cannot be used either. However, f is clearly idempotent.

4.2 Question 7

Which subsets of the following properties uniquely specify that f computes the gcd function for all nonnegative integer inputs?

p1 x = f 0 x == x
p2 x y = f x y == f y x
p3 x y = x <= y ==> f x y == f x (y - x)
p4 x y = x <= y ==> f x y == f x (f x y)

✗p1 and p2,
✗p1 and p4,
✔p1, p2 and p3,
✗p1, p2 and p4

We show that p1, p2 and p3 uniquely specify gcd for. Assume that a function f satisfies these properties. Then it obeys the following definition:

f 0 x = x
f x y
  | x > y = f y x
  | otherwise = f x (y - x)

This definition allows us to calculate f for any nonnegative input value of x, y. This is because in every two recursive iterations, the difference between the two inputs decreases.i

The other answers cannot be correct: e.g. the least common multiple function also satisfies all the other properties.

4.3 Question 8

The following code converts Haskell Int values to and from strings containing their hexadecimal representation (as sequences consisting only of the characters '0', '1', '2', '3', '4', '5', '6', '7', '8', '9', 'A', 'B', 'C', 'D', 'E', 'F').

toHex :: Int -> String
toHex 0 = ""
toHex n =
  let
    (d,r) = n `divMod` 16
  in
    toHex d ++ ["0123456789ABCDEF" !! r]

fromHex :: String -> Int
fromHex = fst . foldr eachChar (0,1)
  where
    eachChar c (sum, m) =
      case elemIndex (toUpper c) "0123456789ABCDEF" of
        Just i  -> (sum + i * m, m * 16)
        Nothing -> (sum        , m * 16)

Select all properties that these functions satisfy.

✔i >= 0 ==> fromHex (toHex i) == i,
✔i > 0 ==> length (toHex i) <= length (show i),
✗all (`elem` "0123456789") s ==> read s <= fromHex s,
✔all (`elem` "0123456789ABCDEF") s ==> fromHex s == fromHex ('0':s).

Property 1 is true as converting to a hexadecimal string and then back should result in the same number.

Property 2 is true, as for positive (i.e. nonzero) integers the toHex representation will never be longer than the decimal string representation.

Property 3 is false as read will throw an exception when given the empty list for s.

Property 4 is true, as adding leading zeroes to a hexadecimal number does not change its value.

Footnotes:

: This is not the same as selecting the properties which are true. Which properties are necessary to maintain our data invariants?

Submission is already closed for this quiz. You can click here to check your submission (if any).